B, T:Type, a:Knd, tg:Id, l:IdLnk, f:(B(T List)).
(a = rcv(l,tg)  T = B)  ma-single-sends0(B;T;a;l;tg;f)  MsgA 

latex

Definitions	t  T, a:A fp B(a), Knd, x : v, MsgA, Prop, IdLnk, ma-single-sends0(B;T;a;l;tg;f), with declarations ds:dsda:dak(v) sends f s v on link l, S  T, State(ds), , Id, f(x)?z, f  g, Valtype(da;k), x. t(x), KindDeq, P  Q, rcv(l,tg), x:A. B(x), Top, P  Q, SQType(T), {T}, P  Q, P & Q, x  dom(f), , b, b, A, False, True, Unit
Lemmas	fpf-single-dom, eqof eq btrue, assert wf, not wf, bnot wf, bool wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, bool sq, eqtt to assert, bool cases, rcv wf, Kind-deq wf, Knd wf, fpf-cap-single1, top wf, fpf-single wf, fpf-join-cap-sq, fpf-join wf, fpf-cap wf, ma-valtype wf, Id wf, fpf-empty wf, ma-state wf, ma-single-sends wf, IdLnk wf